In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements are contained (...) in the type of individuals. Russell's paradox is avoided by placing a type-constraint on lambda-abstraction, rather than by restricting comprehension. (shrink)

Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...) and the recent revivals of Π-reduction as in [11, 14], illustrate the elegance of giving Π-redexes a status similar to λ-redexes. However, Π-reduction in the λ-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a Π-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations or let-expressions. We will show that the λ-cube extended with Π-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of Π-reduction. We believe that this extension of the λ-cube is very useful: it gives a full formal study of two concepts that are useful for theorem proving and programming languages. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...) (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.

Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell ’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus. Currently, types and functions are the heart of logic and computation and not only are they so closely intertwined, but their evolution demands that (...) they be treated in the same manner. Both are usually constructed, abstracted over and instantiated and the operations for abstraction, construction, instantiation and substitution act alike on both. This paper aims to give a framework where the relationship between functions and types takes into account the similarity of their construction, abstraction, instantiation and substitution. For such a “types as functions” framework to work, special forms of function abstraction need to be included. (shrink)

In this paper, a theory T H based on combining type freeness with logic is introduced and is then used to build a theory of properties which is applied to determiners and quantifiers.

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...) logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...) Both λσ and λse when extended with eta-reduction rules, have proved useful for solving higher order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that λσ and λse as well as λσ and the suspension calculus are non-comparable while λse is more adequate than the suspension calculus in simulating one-step beta-reduction. After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions , we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the λ-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the λse we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the λσ and λsusp. (shrink)

This paper described a formal theory of type judgments for propositional logic notations of PM; I felt the need of my own automated type checker to check their examples. The type checker I wrote did indeed serve to help me referee the paper, but also took a rather different approach to notation and typing for propositional functions of PM, which proved worth writing up independently in our own paper: Holmes, M. Randall, “Polymorphic type– checking for the ramified theory of types (...) of Principia Mathematica”, in Fairouz Kamareddine, ed., Thirty–five Years of Automating Mathematics, Kluwer, 2003, pp. 173-215. (shrink)

According to historical theories of biological function, a trait's function is determined by natural selection in the past. I argue that, in addition to historical functions, ahistorical functions ought to be recognized. I propose a theory of biological function which accommodates both. The function of a trait is the way it contributes to fitness and fitness can only be determined relative to a selective regime. Therefore, the function of a trait can only be specified relative to a selective regime. Apart (...) from its desirable pluralism, only this view of relational function can support the function/accident and function/malfunction distinctions commonly thought to be part of the concept of function. Furthermore, only relational function correctly characterizes the explanatory consequences of function attributions in evolutionary biology. (shrink)

A record of the words and teachings of Confucius, _The Analects_ is considered the most reliable expression of Confucian thought. However, the original meaning of Confucius's teachings have been filtered and interpreted by the commentaries of Confucianists of later ages, particularly the Neo-Confucianists of the Song dynasty, not altogether without distortion.In this monumental translation by Professor D. C. Lau, an attempt has been made to interpret the sayings as they stand. The corpus of the sayings is taken as an organic (...) whole and the final test of the interpretation rests on the internal consistency it exhibits. In other words, _The Analects_ is read in the light of _The Analects._This results in a truer understanding of Confucius' thought than the traditional interpretation and paves the way for a re-assessment of its importance in the history of Chinese thought and its relevance to the present day world.This volume also contains an introduction to the life and teachings of Confucius, and three appendices on the events in the life of Confucius, on his disciples, and on the composition of _The Analects._. (shrink)

Tradition, Rationality and Virtue provides the first comprehensive and detailed treatment of the work of Alasdair MacIntyre. In this book, Thomas D'Andrea presents an accessible critical study of the full range of MacIntyre's thought, across ethical theory, psychoanalytic theory, social and political philosophy, Marxist theory, and the philosophy of religion. Moving from the roots of MacIntyre's thought in ethical inquiry, this book examines MacIntyre's treatment of Marx, Christianity, and the nature of human action and discusses in depth the development and (...) applications of MacIntyre's After Virtue project. The book culminates in an examination of major internal and external criticisms of MacIntyre's work and a consideration of its future directions. (shrink)

It is widely held that quantum mechanics is the first scientific theory to present scientifically internal, fundamental difficulties for a realistic interpretation (in the philosophical sense). The standard (Copenhagen) interpretation of the quantum theory is often described as the inevitable instrumentalistic response. It is the purpose of the present article to argue that quantum theory doesnot present fundamental new problems to a realistic interpretation. The formalism of quantum theory has the same states—it will be argued—as the formalisms of older physical (...) theories and is capable of the same kinds of philosophical interpretation. This result is reached via an analysis of what it means to give a realistic interpretation to a theory. The main point of difference between quantum mechanics and other theories—as far as the possibilities of interpretation are concerned—is the special treatment given tomeasurement by the “projection postulate.” But it is possible to do without this postulate. Moreover, rejection of the projection postulate does not, in spite of what is often maintained in the literature, automatically lead to the many-worlds interpretation of quantum mechanics. A realistic interpretation is possible in which only the reality ofone (our) world is recognized. It is argued that the Copenhagen interpretation as expounded by Bohr is not in conflict with the here proposed realistic interpretation of quantum theory. (shrink)

Contemporary Continental Philosophy steps back from current debates comparing Continental and analytic philosophy and carefully, yet critically outlines the tradition’s main philosophical views on epistemology and ontology. Forgoing obscure paraphrases, D’Amico provides a detailed, clear account and assessment of the tradition from its founding by Husserl and Heidegger to its challenge by Derrida and Foucault. Though intended as a survey of this tradition throughout the twentieth century, this study’s focus is on the philosophical problems which gave it birth and even (...) now continue to shape it.The book reexamines Husserl as an early critic of epistemological naturalism whose grasp of the philosophical importance of the theory of meaning was largely ignored. Heidegger’s contrasting effort to revive ontology is examined in terms of his distinction between ontic and ontological questions. In contrast with many earlier studies, the author outlines confusions engendered by the misappropriation of the distinct philosophical agendas of Husserl and Heidegger by such famous figures as Sartre and Merleau-Ponty. The book is also original in its emphasis on how social externalism in epistemology, inspired by Karl Mannheim, influenced this tradition’s structuralist and Marxist phases. The philosophical defenses of a theory of interpretation by Gadamer and Habermas are closely examined and assessed and the study concludes with a a probing yet balanced account of Foucault and Derrida as critics of philosophical autonomy. The book concludes by reassessing this century-long divide between the analytic and Continental traditions and its implication for the future of philosophy. (shrink)

Chronic pain patients often miss receiving acknowledgement for the multidimensional struggles they face with their specific conditions. People suffering from chronic pain experience a type ofinvisibilitythat is also borne by other chronically ill people and their respective medical conditions. However, chronic pain patients face both passive and active exclusion from social participation in activities like family interactions or workplace inclusion. Although such aspects are discussed in the debates lead by the bio-psycho-social model of pain, there seems to be a lack (...) of a distinct interest in assessing more specifically the social aspects regarding chronic pain. As a result, the social aspects have yet to be taken into a more thorough theoretical consideration of chronic pain and to be practically implemented to help affected patients. By addressing chronic pain patients’ struggle for recognition, this paper attempts to shed light on some of these social aspects. We base this attempt on a theoretical framework that combines patients’ statements with an adaptation of Axel Honneth’s social-philosophical work onrecognition. Thus, this paper tries to make a suggestion on how the bio-psycho-social model of pain can live up to its name by helping to address more adequately some of the more neglected aspects in chronic pain patients’ suffering than has been possible to date. (shrink)

In philosophical interpretations of the Laozi the function of the ‘sage’ is a relatively under concentrated on topic. Although nearly every scholar does have something to say about the sage, comments are usually brief and often revolve around the sage as some particular character-type; for example highlighting the sage as a ‘sage-ruler’. In this article we will argue that the sage serves as a tool for understanding the major concepts, thinking, and logic of the Laozi. While the sage does often (...) refer to the sage-ruler this does not mean all references are politically orientated, and even those that are can easily be applied to a host of social situations. This paper thus seeks to appreciate the context for what the Laozi says by looking at how the text itself envisions the embodiment of its ideas through reference to the sage. (shrink)

Several authors, including Thomas Nagel and David Gauthier, have defended the view that reasons of self-interest (prudential reasons) are rationally binding. That is, there is always a reason, bearing on the rational advisability, based on one's self-interest and, as a result, a person may act irrationally by knowingly acting against such reasons regardless of the person's desires or values. Both Nagel and Gauthier argue from the rationally mandatory nature of prudential reasons to the conclusion that moral reasons can be rationally (...) mandatory, challenging the neo-Humean position that practical reasons that bear on an agent's rationality are essentially grounded on the agent's subjective, contingent, conative states. I argue, pace Nagel and Gauthier, that prudential reasons are not rationally mandatory--that the rational requirement to act in one's own interest, when it exists, is, as the neo-Humean insists, grounded on one's subjective, contingent, conative states. Prudential reasons are not reasons for every (conceivable) agent--not in the sense that bears on the rational advisability of action. (shrink)

A study was carried out from October, 2020 to September, 2021to investigate the diversity of fishes and the conservation status of Chittaura Jheel (Bahraich), Uttar Pradesh. During the study period, 38 fish species belonging to 28 genera, 14 families and 7 orders have been identified. The order Cypriniformes was found the dominated order with 15 species(39.47%) followed by Siluriformes 10 species (26.31%), Perciformes 4 species (10.52%), Ophiocephaliformes 4 species (10.52%), Synbranchiformes2 species (5.26%), Osteoglossiformes 2 species (5.26%) and Clupiformes 1 species (...) (2.63 %), The present investigation showed that the wetland, Chittaura Jheel possesses rich fish biodiversity but proper conservation measures are required to maintain sustainability and richness of the fish species diversity of that wetland of U.P. According to IUCN, 30 were enlisted as Least Concern (LC), 2 species as near endangered (NE), 3 species as near threatened (NT), 2 listed as Endangered (EN) and 1 species was listed as Vulnerable (VU). There is a need of conservation of fish diversity of this natural wetland. The pressure is increasing day by day due to increasing population, leading to loss of fish diversity hence identifying the problem and making a better management plan is the way for conservation of the fish diversity of the Chittaura Jheel, a wetland of Bahraich district of Uttar Pradesh. (shrink)

?Are the reasons for acting also the causes of action?? When this question was asked in the early 1960s it received by and large a negative reply: ?No, reasons are not causes?. Yet, when the same question ?Are the reasons for acting the causes of action?? is posed some twenty years later, the predominant answer is ?Yes, reasons are causes?. How could one and the same question receive such diverging answers in the space of only a couple of decades? This (...) paper argues that the shift from an anti-causalist to a causalist consensus is not fully accounted for by the results of first-order debates in the philosophy of action and is owing instead to a change in second-order meta-philosophical assumptions concerning the role and character of philosophical analysis. (shrink)

In 1999, da Silva, D'Ottaviano and Sette proposed a general definition for the term translation between logics and presented an initial segment of its theory. Logics are characterized, in the most general sense, as sets with consequence relations and translations between logics as consequence-relation preserving maps. In a previous paper the authors introduced the concept of conservative translation between logics and studied some general properties of the co-complete category constituted by logics and conservative translations between them. In this paper we (...) present some conservative translations involving classical logic, Lukasiewicz three-valued system L3, the intuitionistic system I1 and several paraconsistent logics, as for instance Sette's system P1, the D'Ottaviano and da Costa system J3 and da Costa's systems Cn, 1≤ n≤ω. (shrink)

This volume collects essays by philosophers and scholars working at the interface of Western philosophy and Buddhist Studies. Many have distinguished scholarly records in Western philosophy, with expertise in analytic philosophy and logic, as well as deep interest in Buddhist philosophy. Others have distinguished scholarly records in Buddhist Studies with strong interests in analytic philosophy and logic. All are committed to the enterprise of cross-cultural philosophy and to bringing the insights and techniques of each tradition to bear in order to (...) illuminate problems and ideas of the other. These essays address a broad range of topics in the philosophy of mind, philosophy of language, logic, epistemology, and metaphysics, and demonstrate the fecundity of the interaction between the Buddhist and Western philosophical and logical traditions. (shrink)

Chez les commentateurs platoniciens de l’époque impériale, l’un des problèmes majeurs liés à la théorie des Idées concernait le domaine d’application de cette doctrine. L’exégèse de la première partie du Parménide de Platon donnait occasion à diverses discussions sur ce sujet. Le Commentaire de Proclus sur le Parménide est sans doute la plus précieuse source qui soit parvenue de l’Antiquité jusqu’à nous pour la reconstitution de ces débats. Alors que la grande majorité des commentateurs anciens étaient convaincus que les Idées (...) ont un domaine assez restreint, le Commentaire de Proclus nous révèle l’existence d’une lecture alternative, selon laquelle il y a des Idées de « toutes choses ». Proclus relie cette interprétation alternative en particulier à l’existence des Idées de choses mauvaises et d’individus, probablement parce que ces deux classes d’objets étaient vraiment les dernières choses dont un platonicien orthodoxe voudrait admettre des Idées. Amélius est le seul néoplatonicien connu pour avoir soutenu l’existence des Idées de choses mauvaises. Dans cet article j’essaie de montrer que, selon toute vraisemblance, Amélius est également la cible de la réfutation des Idées d’individus par Proclus dans son Commentaire. La conclusion qui s’ensuit naturellement est qu’Amélius était très probablement l’un de ces philosophes qui, d’après Proclus, admettaient des Idées « de toutes choses ». (shrink)

Inappropriate authorship is a common problem in biomedical research and may be becoming one in bioethics, due to the increase in multiple authorship. This paper investigates the authorship policies of bioethics journals to determine whether they provide adequate guidance for researchers who submit articles for publication, which can help deter inappropriate authorship. It was found that 63.3% of bioethics journals provide no guidance on authorship; 36.7% provide guidance on which contributions merit authorship, 23.3% provide guidance on which contributions do not (...) merit authorship, 23.3% require authors to take responsibility for their contributions or for the article as a whole, 20% provide guidance on which contributions merit an acknowledgement but not authorship, 6.7% require authors to describe their contributions, and only 3.3% distinguish between authorship in empirical and conceptual research. To provide authors with effective guidance and promote integrity in bioethics research, bioethics journals should adopt authorship policies that address several important topics, such as the qualifications for authorship, describing authorship contributions, taking responsibility for the research and the difference between authorship in empirical and conceptual research. (shrink)

A laboratory-testable, solid-state Maxwell demon is proposed that utilizes the electric field energy of an open-gap p-n junction. Numerical results from a commercial semiconductor device simulator (Silvaco International–Atlas) verify primary results from a 1-D analytic model. Present day fabrication techniques appear adequate for laboratory tests of principle.

D. A. Lloyd Thomas; VIII—Political Decision Procedures1, Proceedings of the Aristotelian Society, Volume 70, Issue 1, 1 June 1970, Pages 141–160, https://doi.or.

What has become known asthe blockers problemis an alleged difficulty facing attempts to formulate physicalism as a supervenience thesis. A blocker is an entity, itself contrary to physicalism, with the power to disrupt an otherwise necessary connection between physical and nonphysical conditions. I argue that there is no distinct blockers problem. Insofar as a problem can be identified, it turns out to be just a rather baroque version of a distinct and familiar objection to supervenience formulations and to be of (...) no independent interest. Work on the formulation of physicalism can thus proceed without worrying about blockers. (shrink)

In Bester’s article (2018) challenging the use of the harm principle and advocating sole reliance on the use of a best interest standard (BIS) in pediatric decision-making, we believe that the auth...

This book contains a rich, interdisciplinary collection of articles by some of the pioneers of contemporary research on attention.

Accepting James Gustafson's recent argument that right reading and valid criticism of H. R. Niebuhr's Christ and Culture must begin with an informed understanding of Niebuhr's utilization of the ideal-typical method, the author reviews characteristics of Weberian typologies and discusses the levels of criticism to which typologies are legitimately subject. Right appreciation of the text's genre exposes many criticisms of Christ and Culture to be misguided, but it also throws into relief those features of the text that cannot be accounted (...) for by that method, revealing the complexity of a text that advances both a comparative descriptive analysis and a bold theological argument. Recognition of this tension prompts the question whether the one so compromises or constrains the other that the enterprise does, indeed, fail as a whole, even though it remains intensely interesting in all its parts. (shrink)

Building on Jean-Luc Marion's phenomenology of love this book takes up the "question of the Other" and argues that through the interpretive activities of the amorous imagination lovers come to experience one another as the Beloved.